Eléments de l'association
|  |
List of bibliographic references
Number of relevant bibliographic references: 87.| Ident. | Authors (with country if any) | Title |
|---|---|---|
| 000186 | Stephan Merz [France] ; Hernán Vanzetto [France] | Encoding TLA+ set theory into many-sorted first-order logic |
| 000296 | David Déharbe [Brésil] ; Stephan Merz [France] | Software Component Design with the B Method — A Formalization in Isabelle/HOL |
| 000702 | Carlos Areces [Argentine] ; Pascal Fontaine [France] ; Stephan Merz [France] | Modal Satisfiability via SMT Solving |
| 000829 | Gerald Lüttgen [Allemagne] ; Stephan Merz [France] | Editorial: Special Issue of Automated Verification of Critical Systems |
| 000831 | Gerald Lüttgen [Allemagne] ; Stephan Merz [France] | Science of Computer Programming Special Issue: Automated Verification of Critical Systems |
| 000864 | Jingshu Chen [France] ; Marie Duflot [France] ; Stephan Merz [France] | Analyzing Conflict Freedom For Multi-threaded Programs With Time Annotations |
| 000893 | Stephan Merz [France] ; Jun Pang [Luxembourg (pays)] | Formal Methods and Software Engineering – 16th International Conference on Formal Engineering Methods (ICFEM 2014) |
| 000A24 | Damien Doligez [France] ; Jael Kriener [France] ; Leslie Lamport [États-Unis] ; Tomer Libal [France] ; Stephan Merz [France] | Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics |
| 000D21 | Stephan Merz [France] ; Hernán Vanzetto [France] | Refinement Types for TLA+ |
| 001134 | Etienne Mabille [France] ; Marc Boyer [France] ; Loic Féjoz [France] ; Stephan Merz [France] | Certifying Network Calculus in a Proof Assistant |
| 001201 | Bernadette Charron-Bost [France] ; Stephan Merz [France] ; Andrey Rybalchenko [Allemagne] ; Josef Widder [Autriche] | Formal Verification of Distributed Algorithms |
| 001464 | Etienne Mabille [France] ; Marc Boyer [France] ; Loïc Fejoz [France] ; Stephan Merz [France] | Towards Certifying Network Calculus |
| 001975 | Stephan Merz [France] ; Hernán Vanzetto [France] | Harnessing SMT Solvers for TLA+ Proofs |
| 001987 | Tianxiang Lu [France] ; Stephan Merz [France] ; Christoph Weidenbach [France] | Formal Verification Of Pastry Using TLA+ |
| 001A46 | Henri Debrat [France] ; Stephan Merz [France] | Verifying Fault-Tolerant Distributed Algorithms in the Heard-Of Model |
| 001A54 | Pascal Fontaine [France] ; Stephan Merz [France] ; Christoph Weidenbach [Allemagne] | Combination of disjoint theories: beyond decidability |
| 001B58 | Stephan Merz [France] | Stuttering Equivalence |
| 001C21 | Stephan Merz [France] ; Hernán Vanzetto [France] | Automatic Verification Of TLA+ Proof Obligations With SMT Solvers |
| 002197 | Stephan Merz [France] ; Hernán Vanzetto [France] | Towards certification of TLA+ proof obligations with SMT solvers |
| 002202 | Pascal Fontaine [France] ; Stephan Merz [France] ; Bruno Woltzenlogel Paleo [France] | Compression of Propositional Resolution Proofs via Partial Regularization |
| 002203 | David Déharbe [Brésil] ; Pascal Fontaine [France] ; Stephan Merz [France] ; Bruno Woltzenlogel Paleo [France] | Exploiting Symmetry in SMT Problems |
| 002318 | Stephan Merz [France] ; Martin Quinson [France] ; Cristian Rosa [France] | SimGrid MC: Verification Support for a Multi-API Simulation Platform |
| 002327 | Stephan Merz [France] ; Tianxiang Lu [Allemagne] ; Christoph Weidenbach [Allemagne] | Towards Verification of the Pastry Protocol using TLA+ |
| 002618 | Tianxiang Lu [Allemagne, France] ; Stephan Merz [France] ; Christoph Weidenbach [Allemagne] | Towards Verification of the Pastry Protocol Using TLA + |
| 002696 | Bernadette Charron-Bost [France] ; Henri Debrat [France] ; Stephan Merz [France] | Formal Verification of Consensus Algorithms Tolerating Malicious Faults |
| 002791 | Sabina Akhtar [France] ; Stephan Merz [France] ; Martin Quinson [France] | A High-Level Language for Modeling Algorithms and Their Properties |
| 002968 | Sabina Akhtar [France] ; Stephan Merz [France] ; Martin Quinson [France] | A High-Level Language for Modeling Algorithms and their Properties |
| 002A46 | Dominique Méry [France] ; Stephan Merz [France] | Integrated Formal Methods |
| 002A70 | Cristian Rosa [France] ; Stephan Merz [France] ; Martin Quinson [France] | A Simple Model of Communication APIs - Application to Dynamic Partial-order Reduction |
| 002B00 | Tianxiang Lu [Allemagne] ; Stephan Merz [France] ; Christoph Weidenbach [Allemagne] | Model Checking the Pastry Routing Protocol |
| 002B50 | Hehua Zhang [République populaire de Chine] ; Stephan Merz [France] ; Ming Gu [République populaire de Chine] | Specifying and Verifying PLC systems with TLA+: a case study |
| 002B72 | Kaustuv Chaudhuri [France] ; Damien Doligez [France] ; Leslie Lamport [États-Unis] ; Stephan Merz [France] | Verifying Safety Properties With the TLA+ Proof System |
| 002B78 | Pascal Fontaine [France] ; Stephan Merz [France] ; Bruno Woltzenlogel Paleo [France] | Exploring and Exploiting Algebraic and Graphical Properties of Resolution |
| 002D94 | Henri Debrat [France] ; Bernadette Charron-Bost [France] ; Stephan Merz [France] | Formal Verification of Consensus Algorithms in a Proof Assistant |
| 002D99 | Sabina Akhtar [France] ; Stephan Merz [France] ; Martin Quinson [France] | Extending PlusCal: A Language for Describing Concurrent and Distributed Algorithms |
| 003437 | Alexander Schimpf ; Stephan Merz [France] ; Jan-Georg Smaus | Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL |
| 003439 | Francisco L Pez Fraguas [Espagne] ; Stephan Merz [France] ; Juan Rodríguez Hortalá [Espagne] | A Formalization of the Semantics of Functional-Logic Programming in Isabelle |
| 003462 | David Déharbe [Brésil] ; Pascal Fontaine [France] ; Anamaria Martins Moreira [Brésil] ; Stephan Merz [France] ; Anderson Santana De Oliveira | Automating model-based software engineering |
| 003523 | Cristian Rosa [France] ; Martin Quinson [France] ; Stephan Merz [France] | Model-checking Distributed Applications with GRAS |
| 003773 | Bernadette Charron-Bost [France] ; Stephan Merz [France] | Formal Verification of a Consensus Algorithm in the Heard-Of Model |
| 003A25 | Mouna Chaouch-Saad [Tunisie] ; Bernadette Charron-Bost [France] ; Stephan Merz [France] | A Reduction Theorem for the Verification of Round-Based Distributed Algorithms |
| 003C62 | Cristian Rosa [France] ; Martin Quinson [France] ; Stephan Merz [France] | Model-checking Distributed Applications with GRAS |
| 003F16 | Loïc Fejoz [France] ; Stephan Merz [France] | Towards automatic proofs of lock-free algorithms |
| 004513 | Stephan Merz [France] | The Specification Language TLA+ |
| 004519 | Fred Kröger [Allemagne] ; Stephan Merz [France] | Temporal Logic and State Systems |
| 004551 | Stephan Merz [France] ; Nicolas Navet [France] | Modeling and Verification of Real-Time Systems - Formalisms and Software Tools |
| 004555 | Serge Autexier [Allemagne] ; Heiko Mantel [Allemagne] ; Stephan Merz [France] ; Tobias Nipkow [Allemagne] | Journal of Automated Reasoning Special Issue: Formal Modeling and Verification of Critical Systems |
| 004602 | Stephan Merz [France] | An introduction to model checking |
| 004840 | Clément Hurlin ; Amine Chaib ; Pascal Fontaine [France] ; Stephan Merz [France] ; Tjark Weber | Practical Proof Reconstruction for First-order Logic and Set-Theoretical Constructions |
| 004872 | Loïc Fejoz [France] ; Stephan Merz [France] | Dérivation d'algorithmes sans verrou à partir d'une spécification atomique |
| 004C00 | Eun-Young Kang [France] ; Stephan Merz [France] | Predicate diagrams for the verification of real-time systems |
| 004E32 | Dominique Méry [France] ; Stephan Merz [France] | Specification and Refinement of Access Control |
| 004E44 | Stephan Merz [France] ; Tobias Nipkow [Allemagne] | Proceedings of the 6th International Workshop on Automated Verification of Critical Systems (AVoCS 2006) |
| 005165 | Houda Fekih [France] ; Leila Jemni Ben Ayed [Tunisie] ; Stephan Merz [France] | Transformation of B Specifications into UML Class Diagrams and State Machines |
| 005193 | Dominique Méry [France] ; Stephan Merz [France] | Event Systems and Access Control |
| 005484 | Pascal Fontaine [France] ; Jean-Yves Marion [France] ; Stephan Merz [France] ; Leonor Prensa Nieto [France] ; Alwen Tiu [France] | Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants |
| 005589 | Alexander Knapp [Allemagne] ; Stephan Merz [France] ; Martin Wirsing [Allemagne] ; Julia Zappe [Allemagne, France] | Specification and refinement of mobile systems in MTLA and mobile UML |
| 005632 | Stephan Merz [France] | Model checking : éléments de base |
| 005915 | Eunyoung Kang [France] ; Stephan Merz [France] | Predicate Diagrams for the Verification of Real-Time Systems |
| 005A62 | Moritz Hammer [Allemagne] ; Alexander Knapp [Allemagne] ; Stephan Merz [France] | Truly On-The-Fly LTL Model Checking |
| 005A67 | Loïc Fejoz [France] ; Dominique Méry [France] ; Stephan Merz [France] | DIXIT: a Graphical Toolkit for Predicate Abstractions |
| 005F61 | Loïc Fejoz ; Dominique Méry [France] ; Stephan Merz | DIXIT : a Graphical Toolkit for Predicate Abstractions |
| 006165 | Moritz Hammer [Allemagne] ; Alexander Knapp [Allemagne] ; Stephan Merz [France] | Truly On-the-Fly LTL Model Checking |
| 006B43 | Alexander Knapp [Allemagne] ; Stephan Merz [France] ; Martin Wirsing [Allemagne] | Refining Mobile UML State Machines |
| 006D28 | Alexander Knapp ; Stephan Merz [France] ; Martin Wirsing | Refining Mobile UML State Machines |
| 006D55 | Houda Fekih [France] ; Leila Jemni ; Stephan Merz [France] | Transformation des spécifications B en des diagrammes UML |
| 006E74 | Stephan Merz [France] | TLA+ Case Study: A Resource Allocator |
| 007B09 | Stephan Merz [France] ; Martin Wirsing [Allemagne] ; Júlia Zappe [Allemagne] | A Spatio-Temporal Logic for the Specification and Refinement of Mobile Systems |
| 007B53 | Stephan Merz [France] | On the logic of TLA+ |
| 007D33 | Houda Fekih [Tunisie] ; Stephan Merz [France] | Translating B machines into UML diagrams |
| 007D40 | Mohamed El Habib ; Claude Kirchner [France] ; Hélène Kirchner [France] ; Jean-Yves Marion [France] ; Stephan Merz [France] | The QSL platform at LORIA |
| 007D78 | Stephan Merz [France] | On the Logic of TLA+ |
| 007E29 | Stephan Merz [France] ; Ali Sezgin | Emptiness of Linear Weak Alternating Automata |
| 007E92 | Stephan Merz [France] ; Martin Wirsing ; Julia Zappe | A Spatio-Temporal Logic for the Specification and Refinement of Mobile Systems |
| 008F02 | Dominique Cansell [France] ; Dominique Méry [France] ; Stephan Merz | Formal Analysis of a Self-Stabilizing Algorithm - Using Predicate Diagrams |
| 009652 | Dominique Cansell [France] ; Dominique Méry [France] ; Stephan Merz | Formal Analysis of a Self-Stabilizing Algorithm - Using Predicate Diagrams |
| 009B66 | Dominique Cansell [France] ; Dominique Méry [France] ; Stephan Merz | Predicate diagrams |
| 009C29 | Dominique Cansell [France] ; Dominique Méry [France] ; Stephan Merz | Verifying Reactive Systems Using Predicate Diagrams |
| 009C67 | Dominique Cansell [France] ; Dominique Méry [France] ; Stephan Merz | Diagrams Refinement for the Design of Reactive Systems |
| 009C87 | Dominique Cansell [France] ; Dominique Méry [France] ; Stephan Merz | Predicate diagrams for the verification of reactive systems |
| 009F87 | Dominique Cansell [France] ; Dominique Méry [France] ; Stephan Merz [Allemagne] | Predicate diagrams for the verification of reactive systems |
| 00A007 | Dominique Cansell [France] ; Dominique Méry [France] ; Stephan Merz | Predicate diagrams |
| 00A112 | Dominique Cansell [France] ; Dominique Méry [France] ; Stephan Merz | Verifying Reactive Systems Using Predicate Diagrams |
| 00A161 | Dominique Cansell [France] ; Dominique Méry [France] ; Stephan Merz | Predicate diagrams for the verification of reactive systems |
| 00A235 | Dominique Cansell [France] ; Dominique Méry [France] ; Stephan Merz | Diagrams Refinement for the Design of Reactive Systems |
| 00A334 | Yassine Mokhtari [France] ; Stephan Merz | Animating TLA Specifications |
| 00AA41 | Yassine Mokhtari [France] ; Stephan Merz [Allemagne] | Animating TLA Specifications |
| This area was generated with Dilib version V0.6.33. |  |